this was disabled to avoid edge cases where the function
cache would become invalidated as a result of injecting
pate's abstract domain information into macaw

this lack of caching can adversely affect discoverPairs
in cases where many blocks need to be inspected
(since macaw starts over each time)

if we flush the cache for each node (by adding
a flushCache to addOverrides), then we can avoid
this duplicated work without worrying about invalid
cache entries

simplifies the logic required to keep the code discovery
cache valid by instead comparing any current state overrides to
what they were when the retrieved cache entry was created

this avoids the need to explicitly flush the cache whenever
any state override occurs, and consequently allows the cache
to be less conservative

rather than asking the solver to concretize each value individually,
this strategy instead collects all values to be concretized and
concretizes them all at once

in most cases this seems to be an improvement, but there are edge
cases where the batch processing times out and we need to fall back
to the original approach

profiling was enabled

… only some concrete

this relaxes the heuristic slightly to ensure that we attempt to
concretize the contents of a memory cell if it was ever written to
with a concrete value. Previously we attempted to compute a single
abstract domain for the entire cell, which is not always possible.

nothing actually depends on this, for the most part
it just wastes time

a forked instance of the solver has the same assumption context,
and so any results about satisfiability/unsatisfiability can
be re-used by other threads

in practice this turns out to be the most expensive
strategy to try in cases where it doesn't apply

the assumption state in 'envCurrentFrame' is not 100% complete,
as it is missing bounds assumptions for bounded constants

this is a workaround for cases where what4 fails to introduce
this assumption itself